Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

app(nil, k) → k
app(l, nil) → l
app(cons(x, l), k) → cons(x, app(l, k))
sum(cons(x, nil)) → cons(x, nil)
sum(cons(x, cons(y, l))) → sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
sum(plus(cons(0, x), cons(y, l))) → pred(sum(cons(s(x), cons(y, l))))
pred(cons(s(x), nil)) → cons(x, nil)

Q is empty.


↳ QTRS
  ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

app(nil, k) → k
app(l, nil) → l
app(cons(x, l), k) → cons(x, app(l, k))
sum(cons(x, nil)) → cons(x, nil)
sum(cons(x, cons(y, l))) → sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
sum(plus(cons(0, x), cons(y, l))) → pred(sum(cons(s(x), cons(y, l))))
pred(cons(s(x), nil)) → cons(x, nil)

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

app(nil, k) → k
app(l, nil) → l
app(cons(x, l), k) → cons(x, app(l, k))
sum(cons(x, nil)) → cons(x, nil)
sum(cons(x, cons(y, l))) → sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
sum(plus(cons(0, x), cons(y, l))) → pred(sum(cons(s(x), cons(y, l))))
pred(cons(s(x), nil)) → cons(x, nil)

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

app(nil, k) → k
app(l, nil) → l
plus(0, y) → y
pred(cons(s(x), nil)) → cons(x, nil)
Used ordering:
Polynomial interpretation [25]:

POL(0) = 1   
POL(app(x1, x2)) = x1 + 2·x2   
POL(cons(x1, x2)) = x1 + x2   
POL(nil) = 2   
POL(plus(x1, x2)) = x1 + x2   
POL(pred(x1)) = x1   
POL(s(x1)) = 1 + x1   
POL(sum(x1)) = x1   




↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

app(cons(x, l), k) → cons(x, app(l, k))
sum(cons(x, nil)) → cons(x, nil)
sum(cons(x, cons(y, l))) → sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))
plus(s(x), y) → s(plus(x, y))
sum(plus(cons(0, x), cons(y, l))) → pred(sum(cons(s(x), cons(y, l))))

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

app(cons(x, l), k) → cons(x, app(l, k))
sum(cons(x, nil)) → cons(x, nil)
sum(cons(x, cons(y, l))) → sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))
plus(s(x), y) → s(plus(x, y))
sum(plus(cons(0, x), cons(y, l))) → pred(sum(cons(s(x), cons(y, l))))

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

sum(plus(cons(0, x), cons(y, l))) → pred(sum(cons(s(x), cons(y, l))))
Used ordering:
Polynomial interpretation [25]:

POL(0) = 2   
POL(app(x1, x2)) = 2·x1 + x2   
POL(cons(x1, x2)) = x1 + x2   
POL(nil) = 0   
POL(plus(x1, x2)) = x1 + x2   
POL(pred(x1)) = 1 + x1   
POL(s(x1)) = x1   
POL(sum(x1)) = x1   




↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

app(cons(x, l), k) → cons(x, app(l, k))
sum(cons(x, nil)) → cons(x, nil)
sum(cons(x, cons(y, l))) → sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))
plus(s(x), y) → s(plus(x, y))

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

app(cons(x, l), k) → cons(x, app(l, k))
sum(cons(x, nil)) → cons(x, nil)
sum(cons(x, cons(y, l))) → sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))
plus(s(x), y) → s(plus(x, y))

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

app(cons(x, l), k) → cons(x, app(l, k))
sum(cons(x, cons(y, l))) → sum(cons(plus(x, y), l))
Used ordering:
Polynomial interpretation [25]:

POL(app(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(cons(x1, x2)) = 1 + 2·x1 + x2   
POL(nil) = 0   
POL(plus(x1, x2)) = x1 + x2   
POL(s(x1)) = x1   
POL(sum(x1)) = x1   




↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

sum(cons(x, nil)) → cons(x, nil)
sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))
plus(s(x), y) → s(plus(x, y))

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

sum(cons(x, nil)) → cons(x, nil)
sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))
plus(s(x), y) → s(plus(x, y))

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

plus(s(x), y) → s(plus(x, y))
Used ordering:
Polynomial interpretation [25]:

POL(app(x1, x2)) = x1 + x2   
POL(cons(x1, x2)) = x1 + 2·x2   
POL(nil) = 0   
POL(plus(x1, x2)) = 2·x1 + 2·x2   
POL(s(x1)) = 1 + x1   
POL(sum(x1)) = x1   




↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ Overlay + Local Confluence

Q restricted rewrite system:
The TRS R consists of the following rules:

sum(cons(x, nil)) → cons(x, nil)
sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))

Q is empty.

The TRS is overlay and locally confluent. By [19] we can switch to innermost.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ Overlay + Local Confluence
                    ↳ QTRS
                      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

sum(cons(x, nil)) → cons(x, nil)
sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))

The set Q consists of the following terms:

sum(cons(x0, nil))
sum(app(x0, cons(x1, cons(x2, x3))))


Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

SUM(app(l, cons(x, cons(y, k)))) → SUM(app(l, sum(cons(x, cons(y, k)))))
SUM(app(l, cons(x, cons(y, k)))) → SUM(cons(x, cons(y, k)))

The TRS R consists of the following rules:

sum(cons(x, nil)) → cons(x, nil)
sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))

The set Q consists of the following terms:

sum(cons(x0, nil))
sum(app(x0, cons(x1, cons(x2, x3))))

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ Overlay + Local Confluence
                    ↳ QTRS
                      ↳ DependencyPairsProof
                        ↳ QDP
                          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

SUM(app(l, cons(x, cons(y, k)))) → SUM(app(l, sum(cons(x, cons(y, k)))))
SUM(app(l, cons(x, cons(y, k)))) → SUM(cons(x, cons(y, k)))

The TRS R consists of the following rules:

sum(cons(x, nil)) → cons(x, nil)
sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))

The set Q consists of the following terms:

sum(cons(x0, nil))
sum(app(x0, cons(x1, cons(x2, x3))))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 2 less nodes.